\section[Datalog \& LFP]{Datalog \& LFP}
\subsection{Programs}

\begin{frame}
  \frametitle{Datalog and LFP}
  \begin{itemize}
  \item Instead of
    %
    \[ \psi(R,\vecx) \equiv \exists \vecy \bigwedge_i \alpha_i
    (\vecx,\vecy) \]
    %
    \pause write \emph{rule} of form \emph{head} $\ruleif$\emph{body}:
    %
    \[ R_\psi(\vecx) \ruleif \alpha_1 (\vecx,\vecy),\dots,\alpha_m (\vecx,\vecy) \]

    \pause\smallskip
    {\scriptsize Decyphering Libkin's notation: More formally precise, it is
      %
      \[ R_\psi(\vecx) \ruleif \alpha_1 (\vecx\alert{_1},\vecy\alert{_1}),\dots,\alpha_m (\vecx\alert{_m},\vecy\alert{_m}), \]
      %
      where~$\vec{x}$ contains all~$\vec{x_i}$ (and none of the~$\vec{y_i}$).
    }\smallskip
    
  \item Given structure $\fA$, new relation $R_\psi$ contains tuples $\vec{a}$ s.t.
    %
    \[ \fA \models \psi(\vec{a}) \]
    %
    \pause\vspace{-4ex}
  \item E.g.
    %
    \[
    \begin{array}{c}
      R(x_1,x_2) \ruleif E(x_1,y_1), E(y_1,y_2), E(y_2,x_2)\\[1ex]
      \exists y_1 \exists y_2 \big(E(x_1,y_1), E(y_1,y_2), E(y_2,x_1)\big)
    \end{array}
    \]
    %
  \end{itemize}
\end{frame}
\subsection{\Datalog}
\begin{frame}
  \frametitle{\Datalog}
  \vspace{-3ex}
  \begin{itemize}
  \item Recursion: Predicate may appear in body and head of a rule
    %
    \[
    \begin{array}{r@{~~}c@{~}l@{\qquad}l}
      R(x,y) & \ruleif & E(x,y) & (r_1)\\
      R(x,y) & \ruleif & E(x,z), R(z,y) & (r_2)
    \end{array}
    \]
    % 
    \pause seen before as:\quad $E(x,y) \vee \exists z (E(x,z) \wedge trcl(z,y))$
    %
    \smallskip\pause
  \item \defn{\Datalog\ program} over voc. $\sigma$ is a pair~$(\Pi,Q)$, where
    \begin{itemize}
    \item $\Pi$ is a set of rules of form
      %
      \[ P(\vecx) \ruleif \alpha_1 (\vecx,\vecy),\dots,\alpha_m (\vecx,\vecy) \]
      %
    \item $Q$ is a rule head in $\Pi$\smallskip
    \item $P$ not in $\sigma$ \smallskip
    \item $\alpha_i$ atomic formula of form $R(\vecxy)$;~~ $R$ in $\sigma$, or a rule head
    \end{itemize}
    \smallskip
  \pause \item Ex: $(\{(r_1),(r_2)\},\mi{trcl})$
  \end{itemize}
\end{frame}
\subsection{Terminology}
\begin{frame}
  \frametitle{Terminology}
  \begin{itemize}
  \item \emph{Extensional} predicates: relation symbols in $\sigma$
    \bigskip
  \item \emph{Intensional} predicates: heads (not in $\sigma$)
    \begin{itemize}
    \item computed by the program
    \item $Q$ is the \emph{output} (predicate)  
    \end{itemize}
  \end{itemize}
\end{frame}

\subsection{Semantics of \Datalog}
\begin{frame}
  \frametitle{Semantics of \Datalog: Immediate consequence}
  \begin{itemize}
  \item \defn{Immediate consequence} operator \defn{$F_\Pi$} based on~$(\Pi,Q)$:
    \pause
  \item Intensional predicates $P_1,\dots,P_k$, incl.~$Q$. Each $P_i$
    can be defined multiple ($\ell_i$) rules:
    %
    \begin{displaymath}
      \begin{array}{rcl}
        P_i(\vec{x}) & \ruleif & \gamma_1^1(\vec{x},\vec{y_1}),\dots,\gamma_{m_1}^1(\vec{x},\vec{y_1})\\
        \dots & & \dots\\
        P_i(\vec{x}) & \ruleif & \gamma_1^{\ell_i}(\vec{x},\vec{y_{\ell_i}}),\dots,\gamma_{m_{\ell_i}}^{\ell_i}(\vec{x},\vec{y_{\ell_i}})
      \end{array}
    \end{displaymath}
    %
  \pause  
  \item $\fA$;~~sets~$\vec{Y}=(Y_1,\dots,Y_k)$,~~$Y_i \subseteq A^{n_i}$,~~$n_i$ arity of~$P_i$
  \pause
  \item $F_\Pi(\vec{Y})=(Z_1,\dots,Z_k)$, where
  \end{itemize}
  %
  \pause
  \begin{displaymath}
      Z_i = \{ \vec{a} \in A^{n_i} \mid (\fA,Y_1,\dots,Y_k) \models \bigvee_{j=1}^{l_i} \exists \vec{y_j} \big(\gamma_1^j(\vec{a},\vec{y_j}),\dots,\gamma_{m_j}^j(\vec{a},\vec{y_j})\big)\} 
  \end{displaymath}  
\end{frame}
\subsection{Immediate Consequence $F_\Pi$}
\begin{frame}
  \frametitle{Immediate Consequence $F_\Pi$}
  \begin{itemize}
    \item $F_\Pi(Y_1,\dots,Y_k) = (Z_1,\dots,Z_k)$, where
  \end{itemize}
  %
  \begin{displaymath}
      Z_i = \{ \blueAt{5}{\vec{a} \in A^{n_i}} \mid \blueAt{4}{(\fA,Y_1,\dots,Y_k)} \models \blueAt{3}{ \bigvee_{j=1}^{l_i} } \blueAt{2}{\exists \vec{y_j} \big(\gamma_1^j(\vec{a_1},\vec{y_j}),\dots,\gamma_{m_j}^j(\vec{a_{m_j}},\vec{y_j})\big)}\} 
    \end{displaymath}
    \begin{itemize}
      \onslide<2->\item \blueAt{2}{$\exists \vec{y_j} \big(\gamma_1^j(\vec{a},\vec{y_j}),\dots,\gamma_{m_j}^j(\vec{a},\vec{y_j})\big)$} \quad\dots\quad Cond. for rule with head~$P_i$.
      \onslide<3->\smallskip\item \blueAt{3}{$\bigvee_{j=1}^{l_i}$} \quad\dots\quad Take for \emph{any} of the~$\ell_i$ rules for~$P_i$ \dots
      \onslide<4->\smallskip\item \blueAt{4}{$(\fA,Y_1,\dots,Y_k)$} \quad\dots\quad in the expansion of~$\fA$ due to~$(Y_1,\dots,Y_k)$
      \onslide<5->\smallskip\item \blueAt{5}{$\vec{a} \in A^{n_i}$} \quad\dots\quad satisfying head assignments.
    \end{itemize}
\end{frame}

\begin{frame}
  \frametitle{Immediate Consequence $F_\Pi$ (cont'd)}
  \begin{itemize}
  \item Formula $Z_i$ is positive in all intensional predicates
    \smallskip\pause
  \item $\Rightarrow F_\Pi$ is monotone
    \smallskip\pause
  \item $\Rightarrow lpf(F_\Pi) = (P_1^\infty,\dots,P_k^\infty)$
    \smallskip\pause
  \item Output of program~$(\Pi,Q)$ as~$Q^\infty$~~($Q=P_i$ for some~$i$)
    \smallskip\pause
  \item Thus, semantics of Datalog given by simultaneous least fixed point    
  \end{itemize}
  %
  \vspace{1ex}
  \begin{displaymath}
    \psi_i(P_1,\dots,P_k,\vec{x}) \equiv \bigvee_j \exists y_j \big(\gamma_1^j(\vec{x},\vec{y_j}),\dots,\gamma_{m_j}^j(\vec{x},\vec{y_j})\big)
  \end{displaymath}
  %
  \begin{itemize}
    \pause
    \item $\Rightarrow$ Answer to $(\Pi,Q)$ on $\fA$ is, given a system~$\Psi$ of such formulas,
    %
    \[ \{ \veca \mid \fA \models [\lfp_{Q,\Psi}](\veca) \} \]
    %
  \end{itemize}
\end{frame}
\subsection{Expressiveness of Datalog}
\begin{frame}
  \frametitle{Expressiveness of Datalog}
  \begin{itemize}
  \item Thus, Datalog is expressible in \alt<4->{$\LFP=\lfpsimult$}{$\lfpsimult$}
    \smallskip\pause
  \item Do multiple fixed points enrich the expressiveness of the logic?
  \end{itemize}
  %
  \smallskip\pause
  \begin{theorem}
   $\lfpsimult$ = \hbox{LFP}
 \end{theorem}
 
 
 \begin{itemize}
  \onslide<5->\smallskip\item \DatalogMin\ allows atomic formulas $\neg R(\cdot)$, $R \in
    \sigma$ in rule bodies
  \onslide<6->\smallskip\item Int. preds also positive inf \DatalogMin
  \onslide<7->\smallskip\item $\Rightarrow$ $F_\Pi$ also monotone for \DatalogMin
  \onslide<8>\smallskip\item $\Rightarrow$ \DatalogMin\ also expressible in $\LFP$
 \end{itemize}
\end{frame}
\subsection{More results on \Datalog}
\begin{frame}
  \frametitle{More results on \Datalog}
  \begin{itemize}
    \item \defn{Theorem.} \DatalogMin\ $= \exists \LFP$, i.e., restriction of~$\LFP$ where
      \begin{itemize}
      \item $\neg$ can only occur on $R \in \sigma$
      \item $\forall$ not allowed
      \end{itemize}
    \pause\medskip  
    \item Relation to~$\ptime$
      \begin{itemize}
        \pause\smallskip\item \DatalogOptMin\ in~$\ptime$
        \pause\smallskip\item \DatalogOptMin\ can only express monotone
        properties \pause\smallskip\item $\Rightarrow$ cannot
        express~$\ptime$ (even on ordered structures)
        \pause\smallskip\item However:
      \end{itemize}
    \smallskip \item\defn{Theorem.} Over structures
        with successor relation and constants for minimal and maximal
        elements,~\DatalogMin\ captures~$\ptime$  
    \end{itemize}
\end{frame}
\subsection{Other results}
\begin{frame}
  \frametitle{Other results}
  \begin{itemize}
  \item \ifpsimult\ = \IFP~~~and~~~\pfpsimult\ = \PFP
    \medskip
  \item \LFP\ = \IFP~~~(Gurevich-Shelah)
    \medskip
  \item \LFP\ = \IFP\ = $\ptime$~~~ over ordered structures (Immerman-Vardi)
    \medskip
  \item \PFP\ = $\pspace$~~~ over ordered structures
    \bigskip
    \pause \item What about~$\ptime$? (generally)
    \pause
    \begin{itemize}
    \item Conjecture (Gurevich). There is no logic that
      captures~$\ptime$ over the class of all finite structures.
    \pause \item This would imply~$\ptime \neq \text{NP}$ since NP has a logic ($\exists$SO).
    \end{itemize}
  \end{itemize}
\end{frame}

\subsection{Smiley}
\begin{frame}
  \frametitle{Thanks}
  \begin{center}
    \textbf{:)}
  \end{center}
\end{frame}

% stages in trcl example (z)

% lfp before, but result afterwards

% does it exist?

%%% Local Variables:
%%% fill-column: 72
%%% TeX-PDF-mode: t
%%% TeX-debug-bad-boxes: t
%%% TeX-master: "slides"
%%% TeX-parse-self: t
%%% TeX-auto-save: t
%%% reftex-plug-into-AUCTeX: t
%%% End: